T:Type, as:(T List), R:(TTprop{i:l}).
(x:T. R(x,x))  l-ordered(T; x,y.R(x,y); as)  no_repeats(T; as) 

latex

Definitions	t  T, f(a), x(s1,s2), x:A. B(x), P  Q, l-ordered(T; x,y.R(x;y); L), False, A, s = t, prop{i:l}, x:AB(x), void, l_before(x; y; l; T), P  Q, P  Q, P  Q, Type, type List, x,y. t(x;y), no_repeats(T; l)
Lemmas	l-ordered wf, not wf, no repeats iff, l before wf